$\forall$${\it es}$:ES, $i$, $x$:Id, $P$:(vartype($i$;$x$)$\rightarrow$Prop). @$i$ always.$P$($v$) $\in$ Prop